{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, FlexibleInstances,
  FlexibleContexts, MultiParamTypeClasses, UndecidableInstances,
  ScopedTypeVariables, QuasiQuotes, TemplateHaskell #-}

{-# OPTIONS_GHC -fcontext-stack=50 #-}

module Examples.Perfect where

import Data.Type.Equality (cong)
import Type.Ord (EQ)

import Data.Yoko
import Data.Yoko.ReflectBase (DCU)
import Data.Yoko.Cata

import Examples.Eq



data Fork a = Fork a a
instance Eq a => Eq (Fork a) where Fork xL yL == Fork xR yR = xL == xR && yL == yR

data Perfect a = Zero a | Succ (Perfect (Fork a))



data Zero_ a; data Succ_ a



type instance Rep (Zero_ a) = D a :* U
newtype instance RM m (N (Zero_ a)) = RMZero a
instance (EQ ~ Compare a a) => DC (Zero_ a) where
  occName _ = "Zero"
  type Range (Zero_ a) = Perfect a
  fr (RMZero a) = Zero a
instance Generic (Zero_ a) where
  rep (RMZero a) = D a :* U;   obj (D a :* U) = RMZero a

type instance Rep (Succ_ a) = R (Perfect (Fork a)) :* U
newtype instance RM m (N (Succ_ a)) = RMSucc (Med m (Perfect (Fork a)))
instance (EQ ~ Compare a a) => DC (Succ_ a) where
  occName _ = "Succ"
  type Range (Succ_ a) = Perfect a
  fr ~(RMSucc x) = Succ x
instance Generic (Succ_ a) where
  rep (RMSucc x) = R x :* U;   obj (R x :* U) = RMSucc x

instance (EQ ~ Compare a a) => DT (Perfect a) where
  packageName _ = "yoko"
  moduleName _ = "Examples.Perfect"
  type BGU (Perfect a) = PerfectBGU a
  data DCU (Perfect a) dc where
    Zero_ :: DCU (Perfect a) (Zero_ a)
    Succ_ :: DCU (Perfect a) (Succ_ a)
  disband (Zero a) = disbanded $ RMZero a
  disband (Succ x) = disbanded $ RMSucc x
instance (EQ ~ Compare a a) => Universe (DCU (Perfect a)) where
  characteristic u x = case u of
    Zero_ -> x;   Succ_ -> x
instance (a ~ b) => Zero_ b ::: DCU (Perfect a) where inhabits = Zero_
instance (a ~ b) => Succ_ b ::: DCU (Perfect a) where inhabits = Succ_
type instance FinU (DCU (Perfect a)) = EnumU ((:=:) (Zero_ a) :|| (:=:) (Succ_ a))
instance Finite (DCU (Perfect a)) where
  toUni tag = EnumU $ case tag of
    Zero_ -> LeftU Refl;   Succ_ -> RightU Refl
instance EqT (DCU (Perfect a)) where eqT = eqTFin
instance (Zero_ a ::: u, Succ_ a ::: u) => DCU (Perfect a) :=> u where
  weaken = weakenFin

data PerfectBGU a t where
  Perfect__Base :: PerfectBGU a (Perfect (Fork a))
  Perfect__Step :: (False ~ IsEQ (Compare x a)) => PerfectBGU a (Perfect x) -> PerfectBGU a (Perfect (Fork x))

type family Arg1 a
type instance Arg1 (f a) = a

type instance Perfect (Fork x) :::? PerfectBGU a =
  Or (IsEQ (Compare x a)) (Perfect x :::? PerfectBGU a)

instance (EQ ~ Compare a a) => Universe (PerfectBGU a) where
  characteristic u x = case u of
    Perfect__Base -> x;   Perfect__Step u -> characteristic u x

instance (b ~ Fork x, Perfect b ::: PerfectBGU a :? IsEQ (Compare x a)
         ) => Perfect b ::: PerfectBGU a where
  inhabits = inhabitsAnno [qP|IsEQ (Compare b a)|]
instance (EQ ~ Compare x a) => Perfect (Fork a) ::: PerfectBGU a :? True where
  inhabits = Anno Perfect__Base
instance (Perfect x ::: PerfectBGU a
         ) => Perfect (Fork x) ::: PerfectBGU a :? False where
  inhabits = Anno $ Perfect__Step inhabits

instance PerfectBGU (Fork a) :=> PerfectBGU a where
  weaken Perfect__Base = Perfect__Step Perfect__Base
  weaken (Perfect__Step x) = Perfect__Step $ weaken x


--instance (EQ ~ Compare a a, a ~ b) => PerfectBGU a :=> DTOf (PerfectBGU b) where
--  weaken = w id where
--    w :: forall s t. (DTOf (PerfectBGU a) s -> DTOf (PerfectBGU a) t) ->
--         PerfectBGU a s -> DTOf (PerfectBGU a) t
--    w k Perfect__Base = k $ DTOf Perfect__Base
--    w k (Perfect__Step x) = w (k . (undefined :: DTOf (PerfectBGU a) (Perfect (Arg1 s)) -> DTOf (PerfectBGU a) s)) x
--    w k (Perfect__Step x) = w (k . help) x
instance EqT (PerfectBGU a) where
  eqT = w id where
    w :: forall t s x y a. (t :=: s -> x :=: y) ->
         PerfectBGU a t -> PerfectBGU a s -> Maybe (x :=: y)
    w k Perfect__Base Perfect__Base = Just $ k Refl
    w k (Perfect__Step x) (Perfect__Step y) =
      w (k .   cong  .  cong . injectivity) x y
          --    /\       /\        /\
          -- +Perfect  +Fork    -Perfect
    w _ _ _ = Nothing

    injectivity :: forall f a b. f a :=: f b -> a :=: b
    injectivity Refl = Refl

instance (EQ ~ Compare a a, Eq a) => Eq (Perfect a) where (==) = gEq


data PerfectCata a t where -- just adds Perfect a to PerfectBGU a
  Perfect__Zero :: PerfectCata a (Perfect a)
  Perfect__Sib :: PerfectBGU a (Perfect (Fork x)) -> PerfectCata a (Perfect (Fork x))
instance (Perfect x ::: PerfectCata a :? IsEQ (Compare x a)
         ) => Perfect x ::: PerfectCata a where
  inhabits = inhabitsAnno [qP|IsEQ (Compare x a)|]
instance Perfect a ::: PerfectCata a :? True where inhabits = Anno Perfect__Zero
instance (b ~ Fork ex, Perfect b ::: PerfectBGU a
         ) => Perfect b ::: PerfectCata a :? False where
  inhabits = Anno $ Perfect__Sib inhabits

-- TODO I'm stuck on this instance
--instance PerfectCata Char :=> CataU (PerfectCata Char) m where
--  weaken Perfect__Zero = CataU

x = cata (undefined :: Algebras (PerfectCata Char) IdM) (Succ (Succ (Zero (Fork (Fork 'n' 'i') (Fork 'c' 'k')))))


concat `fmap` mapM derive [''Perfect, ''Fork, ''Zero_, ''Succ_]
